r:Rng, a, b:.
(a  b)
 (E:({a..b}|r|), u:|r|. (((r) a  j < b. E(j)) * u) = ((r) a  j < b. E(j) * u)  |r|) 

latex

Definitions	t  T, x:A. B(x), x. t(x), {T}, , x(s), x f y, P  Q, P & Q, P  Q, P  Q, i  j < k, False, A, A  B, {i..j}, {i...}, Rng
Lemmas	rng wf, int upper ind, int upper wf, rng sum wf, rng times wf, rng car wf, int seg wf, int le to int upper, rng sum unroll base, rng zero wf, rng times zero, rng times over plus, le wf, rng plus wf, rng sum unroll hi